$LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
require 'ext_pr1_v4'

# Uhr mit drei verschiedenen Implementationen und der Möglichkeit verschiedener
# Umrechnungen in 5 Einzelschritten
# 
# clock24   == 24 Stunden Zeitanzeige
# clock12   == 12 Stunden AM und PM Anzeige
# clockSec  == Zeitanzeige in Sekunden

MIN_IN_SEC = 60
HOUR_IN_MIN = 60
DAY_IN_HOUR = 24
HOUR_IN_SEC = HOUR_IN_MIN * MIN_IN_SEC
DAY_IN_SEC = DAY_IN_HOUR * HOUR_IN_SEC
HALF_DAY_IN_SEC = DAY_IN_SEC / 2
HALF_DAY = DAY_IN_HOUR/2

 # Die Klasse Objekt die alle Fälle als FALSE implementiert hat
 
class Object
 def clock?() 
   self.clock_sec? or self.clock_24? or self.clock_12?
 end
 def day_sec?() false end
 def hour24?() false end
 def hour12?() false end
 def halve?() false end
 def min?() false end
 def sec?() false end
 def clock_sec?() false end
 def clock_24?() false end
 def clock_12?() false end
end
  
# Die Klassen für die Einzelfälle
# Überprüfung auf day_sec?
class Integer
 def day_sec?()
   self.int? and self.in?(0...DAY_IN_SEC)
 end
#Überprüfung auf hour24?
 def hour24?()
   self.int? and self.in?(0...DAY_IN_HOUR)
 end
#Überprüfung auf hour12?
 def hour12?()
   self.int? and self.in?(0...(HALF_DAY))
 end
#Überprüfung auf min
 def min?()
   self.int? and self.in?(0...HOUR_IN_MIN)
 end
#Überprüfung auf sec
 def sec?()
   self.int? and self.in?(0...MIN_IN_SEC)
 end
end

# Schritte:
# Schritt 1: 
# Sekundenuhr
# 
# ClockSec ::= ClockSec[:day_sec] :: SecDay

 def_class(:ClockSec,[:day_sec]){
   def invariant?() 
    day_sec.day_sec?
   end
   
  # clock_sec_add ::= (sec1, sec2) :: Nat x Nat -> Nat
  # Test {(21, 19) = 40, (21, -19) = Err }
  def add(sec2)
    check_pre((sec2.clock_sec?))
     ClockSec[self.day_sec + sec2.day_sec]
  end
  
  def to_clock_sec()
    self.day_sec
  end
  
  
  def clock_sec?()
    true
  end
  # clock_sec_sub ::= (sec1, sec2) :: Nat x Nat -> Nat
  # Test {(21, 19) = Err, (19, 21) = 2 }

  def clock_sub(sec2)
    check_pre((sec2.clock_sec? and self.day_sec >= sec2.day_sec))
    ClockSec[self.day_sec - sec2.day_sec]
  end
  
  # clock_sec_succ ::= (sec) :: Nat -> Nat
  # Test { (18) = 19, (18.0) = Err } 

  def clock_succ() 
    ClockSec[self.day_sec.succ()]
    
  end
  
  # clock_sec_pred ::= (sec) :: Nat -> Nat
  # Test { (18) = 17, (18.0) = Err }

  def clock_pred()
    ClockSec[self.day_sec.pred()]
  end
  
  #Konvertierung von ClockSec zu Clock24
  # clock_sec_to_clock_24 ::= (clock) :: ClockSec <-> Clock24
  # Test {clock_sec_to_clock_24(ClockSec[43200]=>Clock24[12,0,0], 
  # clock_sec_to_clock24(ClockSec[86400])=>Err}

  def to_clock_24()
    check_pre((self.clock_sec?))
    hour24, hour_carry = self.day_sec.divmod(HOUR_IN_SEC)
    min, sec = hour_carry.divmod(MIN_IN_SEC)

    Clock24[hour24, min, sec]
  end
  
  #Konvertierung von ClockSec zu Clock12
  #clock_sec_to_clock_12 ::= (clock) :: ClockSec <-> Clock12
  # Test {clock_sec_to_clock_12(ClockSec[43200])=>Clock12[:AM,12,0,0],
  # clock_sec_to_clock12(ClockSec[86400])=>Err }

  def to_clock_12()
    
    clock24 = self.to_clock_24
    
    halve = (clock24.hour24 / HALF_DAY) == 1 ? :PM : :AM
    hour = clock24.hour24 > HALF_DAY ? clock24.hour24 - HALF_DAY : clock24.hour24
    
    Clock12[halve, hour, clock24.min, clock24.sec]
  end
  
  def from(clock)
    check_pre((clock.clock?))
    clock.to_clock_sec
  end
  
  def clock_sec
    self.day_sec
  end
  
  def clock_min
    self.to_clock_24().min
  end
  
  def clock_hour24
    self.to_clock_24().hour24
  end
  
  def clock_hour12
    self.to_clock_12().hour12
  end
  
  def clock_halve
    self.to_clock_12().halve
  end
  
 }

#Schritt 2:
#24 Stunden Uhr
#
# Clock24 ::= Clock24[hour24,min,sec] :: Hour24 x Min x Sec
#
def_class(:Clock24,[:hour24,:min,:sec]){
  def invariant?()
    hour24.hour24? and min.min? and sec.sec?
  end
  #Schritt 3:
  #Konvertierung von Clock24 zu ClockSec
  # clock_24_to_clock_sec ::= (clock) :: Clock24 <-> ClockSec
  # Test { (Clock24[1, 0, 0]=>3600, Clock24[24, 0, 0]=>Err}
  
  def to_clock_sec()
    sec_temp1 = self.hour24 * HOUR_IN_SEC
    sec_temp2 = self.min * MIN_IN_SEC
    sec_temp3 = self.sec
    ClockSec[sec_temp1 + sec_temp2 + sec_temp3]
  end
  
  def from(clock)
    check_pre((clock.clock?))
    clock.to_clock_24()
  end
  
  def clock_24?
    true
  end
  
  #Konvertierung von Clock 24 auf Clock 12
  #clock_24_to_clock_12 ::= (clock) :: Clock24 <-> Clock12
  # Test {clock_24_to_clock_12(Clock24[12,0,0])=>Clock12[:AM,12,0,0], 
  # clock_24_to_clock_12(Clock24[24,0,0])=>Err}
  
  def to_clock_12()
    self.to_clock_sec().to_clock_12()
  end
  
    #Schritt 5
#
# 
# clock_add ::= (clock1,clock2) ::
#                               (Clock24 x Clock -> Clock24 |
#                                Clock12 x Clock -> Clock12 |
#                                ClockSec x Clock -> ClockSec)
# Test { clock_add(ClockSec[39600], clock_add(Clock24[11,0,0],Clock12[:AM,13,0,0]))=>Err}

def add(value)
  check_pre((value.clock?))
  Clock_Sec[self.to_clock_sec + value.to_clock_sec].to_clock_24()
end

  #clock_sub ::= (clock1,clock2) ::
  #                               (Clock24 x Clock -> Clock24 |
  #                                Clock12 x Clock -> Clock12 |
  #                                ClockSec x Clock -> ClockSec)
  # Test { clock_sub(ClockSec[39600]clock_sub(Clock24[11,0,0],Clock12[:AM,13,0,0]))=>Err}

 def clock_sub(value)
  check_pre((value.clock?))
  Clock_Sec[self.to_clock_sec - value.to_clock_sec].to_clock_24()
end

  #clock_pred ::= (clock) ::
  #                         (Clock24 <-> Clock24 |
  #                          Clock12 <-> Clock12 |
  #                          ClockSec <-> ClockSec)
  #
  #Test {clock_pred(ClockSec[39601])=>ClockSec[39600],clock_pred(Clock12[:AM,1,0,1])=>Clock12[:AM,1,0,0],
  # clock_pred(Clock24[1,0,1])=>Clock24[1,0,0], clock_pred(Clock12[:AM,13,0,0])=>Err}

  def clock_pred() 
    self.to_clock_sec().clock_pred().to_clock_24()
  end
  
  #clock_succ ::= (clock) ::
  #                       (Clock24 <-> Clock24 |
  #                        Clock12 <-> Clock12 |
  #                        ClockSec <-> ClockSec)
  #
  #Test {clock_succ(ClockSec[39600])=>ClockSec[39601],clock_succ(Clock12[:AM,1,0,0])=>Clock12[:AM,1,0,1],
  # clock_succ(Clock24[1,0,0])=>Clock24[1,0,1], clock_succ(Clock12[:AM,13,0,0])=>Err}

  def clock_succ() 
    to_clock_sec().clock_sec_succ().to_clock_24()
  end 
  
  def clock_sec
    self.day_sec
  end
  
  def clock_min
    self.min
  end
  
  def clock_hour24
    self.hour24
  end
  
  def clock_hour12
    self.to_clock_12().hour12
  end
  
  def clock_halve
    self.to_clock_12().halve
  end
}
  
  #12 Stunden Uhr
  #
  # Clock12 ::= Clock12[halve,hour12,min,sec] :: Halve x Hour12 x Min x Sec
def_class(:Clock12,[:halve,:hour12,:min,:sec]){
  def invariant?()
   self.halve? and hour12.hour12? and min.min? and sec.sec?
  end
  
 #Überprüfung auf halve
 def halve?()
   self.halve == :AM or self.halve == :PM
 end
 
 def clock_12?
   true
 end
 
 
  #Konvertierung von Clock12 zu ClockSec
  # clock_12_to_clock_sec ::= (clock) :: Clock12 <-> ClockSec
  # Test {Clock12[:AM, 1, 0, 0]=>3600, Clock12[:AM, 13, 0, 0]=>Err}
  
  def to_clock_sec()
    sec_temp1 = ((self.halve == :AM ? 0 : 12) + self.hour12) * HOUR_IN_SEC 
    sec_temp2 = self.min * MIN_IN_SEC
    sec_temp3 = self.sec
    ClockSec[sec_temp1 + sec_temp2 + sec_temp3]
  end
  
  #Konvertierung von Clock 12 auf Clock 24
  #clock_12_to_clock_24 ::= (clock) :: Clock12 <-> Clock24
  # Test {clock_12_to_clock_24(Clock12[:AM,12,0,0])=>Clock24[12,0,0],
# clock_12_to_clock_24(Clock12[:AM,13, 0, 0])=>Err}

def to_clock_24()
  self.to_clock_sec().to_clock_24()
end
  
  #Schritt 5
#
# 
# clock_add ::= (clock1,clock2) ::
#                               (Clock24 x Clock -> Clock24 |
#                                Clock12 x Clock -> Clock12 |
#                                ClockSec x Clock -> ClockSec)
# Test { clock_add(ClockSec[39600], clock_add(Clock24[11,0,0],Clock12[:AM,13,0,0]))=>Err}

def add(value)
  check_pre((value.clock?))
  ClockSec[value.to_clock_sec + self.to_clock_sec].to_clock_12
end

  #clock_sub ::= (clock1,clock2) ::
  #                               (Clock24 x Clock -> Clock24 |
  #                                Clock12 x Clock -> Clock12 |
  #                                ClockSec x Clock -> ClockSec)
  # Test { clock_sub(ClockSec[39600]clock_sub(Clock24[11,0,0],Clock12[:AM,13,0,0]))=>Err}

 def clock_sub(value)
  check_pre((value.clock?))
  ClockSec[value.to_clock_sec - self.to_clock_sec].to_clock_12
end
 
  #clock_pred ::= (clock) ::
  #                         (Clock24 <-> Clock24 |
  #                          Clock12 <-> Clock12 |
  #                          ClockSec <-> ClockSec)
  #
  #Test {clock_pred(ClockSec[39601])=>ClockSec[39600],clock_pred(Clock12[:AM,1,0,1])=>Clock12[:AM,1,0,0],
  # clock_pred(Clock24[1,0,1])=>Clock24[1,0,0], clock_pred(Clock12[:AM,13,0,0])=>Err}
  
  def clock_pred() 
    puts(self.to_clock_sec.clock_pred)
    self.to_clock_sec.clock_pred.to_clock_12
  end
  
  #clock_succ ::= (clock) ::
  #                       (Clock24 <-> Clock24 |
  #                        Clock12 <-> Clock12 |
  #                        ClockSec <-> ClockSec)
  #
  #Test {clock_succ(ClockSec[39600])=>ClockSec[39601],clock_succ(Clock12[:AM,1,0,0])=>Clock12[:AM,1,0,1],
  # clock_succ(Clock24[1,0,0])=>Clock24[1,0,1], clock_succ(Clock12[:AM,13,0,0])=>Err}

  def clock_succ() 
    self.to_clock_sec.succ.to_clock_24.to_clock_12
  end
  
  def clock_sec
    self.day_sec
  end
  
  def clock_min
    self.to_clock_24().min
  end
  
  def clock_hour24
    self.to_clock_24().hour24
  end
  
  def clock_hour12
    self.hour12
  end
  
  def clock_halve
    self.halve
  end

}

#Vergleich von 2 Uhren
#clock_equal? ::= (obj1,obj2) :: (Clock x Clock -> Bool |
#                                 Clock x (Any - Clock) -> False |
#                                (Any - Clock) x Clock -> False |
#                                (Any - Clock) x (Any - Clock) -> Err)

def clock_equal(value1, value2)
  if is_clock(value1) and is_clock(value2) then
    (to_clock_sec(value1) == to_clock_sec(value2))
  elsif not is_clock(value1) or not is_clock(value2) then
    false
  else
    check_pre((false))
  end
end

def is_clock(value)
  (value.clock12? or value.clock24? or value.clock_sec?)
end